Аксиоматика логики

Тут есть варианты. Существует два подхода к описанию логических
вычислителей: гильбертовский вычислитель, генценовский
(последовательный) вычислитель. Разница заключается в том, что
гильбертовский вычислитель обычно состоит из множества аксиом и
одного правила вывода, а последовательный вычислитель состоит из
одной аксиомы и множества правил вывода.

Приведем примеры эквивалентных логик, которыми мы пользуемся ежедневно:

Классическая логика (гильбертовский вычислитель)
Символы: →, ¬, ∧, ∨
Аксиомы: 1. A → ( B → A)
2. (A → (B → C)) → (A → B) → (A → C))
3. A ∧ B → A
4. A ∧ B → B
5. A → (B → (A ∧ B))
6. A → (A ∨ B)
7. B → (A ∨ B)
8. (A → C) → ((B → C) →((A ∨ B) → C))
9. ¬ A → (A → B)
10. (A → B) → ((A → ¬ B) → ¬ A)
11. A ∨ ¬ A
Правило вывода: Modus Ponens (MP)
Замечание: 1. Теория исчисления предикатов первого порядка включает в
себя также правило Generalization (GEN)
2. Если не вкючать последняя 11-ю аксиому исключающего третьего, то
логика превратится в конструктивную.

Компактная теория К (гильбертовский вычислитель)
Символы: →, ¬
Аксиомы: 1. A → ( B → A)
2. (A → (B → C)) → (A → B) → (A → C))
3. (¬ B → ¬ A) → ((¬ B → A) → B)
4. ∀xA(x) →A(y), если y свободно для x в формуле A(x)
5. ∀x(A → B(x)) →(A→∀xB (x)), если A не содержит свободных вхождений x
Правило вывода: Modus Ponens (MP)
Замечание: 1. Теория исчисления предикатов первого порядка включает в
себя также правило Generalization (GEN)
2. Закон исключаещего третьего «прошит» в этой системе.

Генценовская теория LK (последовательный вычислитель)
Символы: →, ¬, ∧, ∨
Аксиома: I
Леммирование: Cut
Правила логики:
1. ∧ L1 8. ∧ R1
2. ∧ L2 9. ∧ R2
3. → L  10. → R
4. ¬ L  11. ¬ R
5. ∀ L  12. ∀ R
6. ∃ L  13. ∃ R
7. ∨ L  14. ∨ R
Правила структурирования:
15. WL 18. WR
16. CL  19. CR
17. PL  20. PR
Замечание: 1. Для того, что бы сделать теорию LK конструктивной (LJ)
нужно изменить только правило 7.